| Definitions | t  T,  x:A. B(x), dt(l;da), lnk-decl(l;dt), Knd, Type,  x.A(x), KindDeq, P   Q,  x. t(x), a:A fp B(a), Top, x:A B(x), x dom(f),  b, f(x), P  Q, P & Q, P Q, x : v, Void,  A, b,  , s = t, Prop, Atom$n, Id, x:A B(x), rec(x.A(x)), ecl(ds;da), msg-spec(ds;da), update-spec(ds;da), update-spec-decl(upd;ds), type List, IdLnk, f || g, left+right, if b t else f fi, False, Unit, f(x)?z, , f  g, reduce(f;k;as),  x:A. B(x), source(l), a = b, msg-spec-links(snd), IdLnkDeq, remove-repeats(eq;L), True, S  T, ecl-tags(l;snd),  T, f(a), x(s), EqDecider(T), ecl-machine3(ds;da;x;T;ks;a;snd), Valtype(da;k), update-spec-vars(upd), ecl-machine2(i;ds;da;x;T;ks;a;upd), "$x", R-da(R;i), R-state-var(i;ds;da;x;T;ks;tr), IdDeq, es realizer ind Rinit compseq tag def, es realizer ind Rplus compseq tag def, let a,b,c,d,e,f,g = u in v(a;b;c;d;e;f;g), ecl-trans-tuple{i:l}(ds;da), ecl-trans(x), R-state-var-init(i;ds;da;x;T;v;ks;tr), ecl-machine1{$ecl:ut2}(i; ds; da; A), ecl-machine at i with state $eclAstate variables dsactions dasends sndupdates upd, {T}, SQType(T), s ~ t, lnk(k), <a,b>, A & B, tag(k), rcv(l,tg) |
| Lemmas | lnk-decl-ap, es-dt-ap, lnk-decl-dom-implies, isrcv-implies, rcv wf, Knd sq, lnk-decl-dom2, lnk wf, tagof wf, IdLnk sq, update-spec-decl wf, update-spec wf, msg-spec wf, ecl wf, ecl-trans wf, ecl-trans-tuple wf, fpf-compatible-single, id-deq wf, R-state-var wf, ecl-machine2 wf, R-da wf, ecl-machine3 wf, R-state-var-da, update-spec-vars wf, ma-valtype wf, R-da-Rall, fpf-compatible wf, squash wf, true wf, deq wf, R-lnk-tags-da, ecl-tags wf, top wf, remove-repeats wf, idlnk-deq wf, msg-spec-links wf, IdLnk wf, ifthenelse wf, not functionality wrt iff, assert-eq-id, eq id wf, Id wf, lsrc wf, fpf-empty-compatible-left, reduce wf, fpf-join wf, fpf wf, fpf-empty wf, fpf-compatible-join2, fpf-cap wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bool wf, bnot wf, not wf, fpf-compatible-single2, fpf-single wf, fpf-compatible-single-iff, fpf-ap wf, assert wf, fpf-dom wf, fpf-trivial-subtype-top, fpf-compatible-symmetry, Kind-deq wf, Knd wf, lnk-decl wf, es-dt wf |
upd:update-spec(ds;da).